A:Type, eq:EqDecider(A), x, y:A, v:Top. x  dom(y : v) ~ (eqof(eq)(y,x)) 

latex

Definitions	eqof(d), Top, EqDecider(T), x : v, x  dom(f), P  Q, Unit, x:A. B(x), t  T,
Lemmas	bool wf, eqof wf, deq wf, top wf